# Contributor: alpine-mips-patches <info@mobile-stream.com>
# Contributor: omni <omni+alpine@hack.org>
# Maintainer: alpine-mips-patches <info@mobile-stream.com>
pkgname=coq
pkgver=8.15.2
pkgrel=0
pkgdesc="A formal proof management system"
url="https://coq.inria.fr"
arch="all !riscv64" # limited by ocaml aport
license="LGPL-2.1-or-later"
depends="ocaml-runtime"
makedepends="ocaml ocaml-findlib ocaml-compiler-libs ocaml-zarith dune ocaml-num-dev bash"
options="!check" # many tests in 'make test-suite' fail
subpackages="$pkgname-doc"
source="$pkgname-$pkgver.tar.gz::https://github.com/coq/coq/archive/V$pkgver.tar.gz"

# 32bit archs
case "$CARCH" in
armv7|armhf|mips|x86) options="$options textrels" ;;
esac

build() {
	./configure \
		-prefix /usr \
		-bytecode-compiler no \
		-coqide no

	case "$CARCH" in
		s390x) OCAMLPATH=/usr/lib/ocaml CAML_LD_LIBRARY_PATH=/usr/lib/ocaml/zarith/ make -j1;;
		*) OCAMLPATH=/usr/lib/ocaml CAML_LD_LIBRARY_PATH=/usr/lib/ocaml/zarith/ make;;
	esac
}

package() {
	make -j1 DESTDIR="$pkgdir" install
}

sha512sums="
6a5487912dedb6e54145bf3f177a091cffe13429ba2f73db7c1cc241fe10e86340c968e19cefba7d680facce55f4e914cbd16a317264b109a6f9a01ec822a8c5  coq-8.15.2.tar.gz
"
